T:Type, P:(T), l:(T List). filter(x.P(x);l)  ({x:T| P(x)}  List) 

latex

Definitions	x:A. B(x), b, t  T, A, b, s = t, , , f(a), x(s), x:AB(x), [car / cdr], P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, {x:A| B(x)} , type List, if b then t else f fi , Type, []
Lemmas	ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf